YES 1.809
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isSuffixOf :: Eq a => [[a]] -> [[a]] -> Bool) :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isSuffixOf :: Eq a => [[a]] -> [[a]] -> Bool) :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isSuffixOf :: Eq a => [[a]] -> [[a]] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy5100), Succ(xy3700000)) → new_primPlusNat(xy5100, xy3700000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy5100), Succ(xy3700000)) → new_primPlusNat(xy5100, xy3700000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy34000), Succ(xy370000)) → new_primMulNat(xy34000, Succ(xy370000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy34000), Succ(xy370000)) → new_primMulNat(xy34000, Succ(xy370000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy3400), Succ(xy37000)) → new_primEqNat(xy3400, xy37000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy3400), Succ(xy37000)) → new_primEqNat(xy3400, xy37000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs2(Left(xy340), Left(xy3700), app(ty_[], gb), gc) → new_esEs(xy340, xy3700, gb)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_Maybe, fa), eh) → new_esEs0(xy340, xy3700, fa)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_@2, bcd), bce), bcb) → new_esEs1(xy341, xy3701, bcd, bce)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_Either, fd), ff), eh) → new_esEs2(xy340, xy3700, fd, ff)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(xy341, xy3701, ed, ee, ef)
new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_[], he)) → new_esEs(xy340, xy3700, he)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_Either, bdg), bdh), bag, bcb) → new_esEs2(xy340, xy3700, bdg, bdh)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(xy342, xy3702, bbf, bbg, bbh)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_[], bah)) → new_esEs(xy342, xy3702, bah)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_Maybe, bcc), bcb) → new_esEs0(xy341, xy3701, bcc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_@2, bde), bdf), bag, bcb) → new_esEs1(xy340, xy3700, bde, bdf)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy340, xy3700, bh, ca, cb)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_[], bdc), bag, bcb) → new_esEs(xy340, xy3700, bdc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_Maybe, bba)) → new_esEs0(xy342, xy3702, bba)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_@2, hg), hh)) → new_esEs1(xy340, xy3700, hg, hh)
new_esEs0(Just(xy340), Just(xy3700), app(ty_Maybe, cd)) → new_esEs0(xy340, xy3700, cd)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_Either, bcf), bcg), bcb) → new_esEs2(xy341, xy3701, bcf, bcg)
new_esEs0(Just(xy340), Just(xy3700), app(ty_[], cc)) → new_esEs(xy340, xy3700, cc)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_[], bca), bcb) → new_esEs(xy341, xy3701, bca)
new_esEs2(Left(xy340), Left(xy3700), app(app(ty_Either, gg), gh), gc) → new_esEs2(xy340, xy3700, gg, gh)
new_esEs2(Left(xy340), Left(xy3700), app(app(app(ty_@3, ha), hb), hc), gc) → new_esEs3(xy340, xy3700, ha, hb, hc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_[], df)) → new_esEs(xy341, xy3701, df)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_[], eg), eh) → new_esEs(xy340, xy3700, eg)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_Either, bbd), bbe)) → new_esEs2(xy342, xy3702, bbd, bbe)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_Maybe, bc)) → new_esEs0(xy340, xy3700, bc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_@2, dh), ea)) → new_esEs1(xy341, xy3701, dh, ea)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_@2, bd), be)) → new_esEs1(xy340, xy3700, bd, be)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(xy341, xy3701, bch, bda, bdb)
new_esEs0(Just(xy340), Just(xy3700), app(app(app(ty_@3, db), dc), dd)) → new_esEs3(xy340, xy3700, db, dc, dd)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), ba) → new_esEs(xy341, xy3701, ba)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_Either, bf), bg)) → new_esEs2(xy340, xy3700, bf, bg)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs1(xy342, xy3702, bbb, bbc)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(app(ty_@3, fg), fh), ga), eh) → new_esEs3(xy340, xy3700, fg, fh, ga)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_@2, fb), fc), eh) → new_esEs1(xy340, xy3700, fb, fc)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_Either, baa), bab)) → new_esEs2(xy340, xy3700, baa, bab)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_Either, eb), ec)) → new_esEs2(xy341, xy3701, eb, ec)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_Maybe, bdd), bag, bcb) → new_esEs0(xy340, xy3700, bdd)
new_esEs2(Left(xy340), Left(xy3700), app(ty_Maybe, gd), gc) → new_esEs0(xy340, xy3700, gd)
new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_Maybe, dg)) → new_esEs0(xy341, xy3701, dg)
new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_Maybe, hf)) → new_esEs0(xy340, xy3700, hf)
new_esEs2(Right(xy340), Right(xy3700), hd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy340, xy3700, bac, bad, bae)
new_esEs0(Just(xy340), Just(xy3700), app(app(ty_@2, ce), cf)) → new_esEs1(xy340, xy3700, ce, cf)
new_esEs2(Left(xy340), Left(xy3700), app(app(ty_@2, ge), gf), gc) → new_esEs1(xy340, xy3700, ge, gf)
new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_[], bb)) → new_esEs(xy340, xy3700, bb)
new_esEs0(Just(xy340), Just(xy3700), app(app(ty_Either, cg), da)) → new_esEs2(xy340, xy3700, cg, da)
new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(xy340, xy3700, bea, beb, bec)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs0(Just(xy340), Just(xy3700), app(app(app(ty_@3, db), dc), dd)) → new_esEs3(xy340, xy3700, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xy340), Just(xy3700), app(app(ty_@2, ce), cf)) → new_esEs1(xy340, xy3700, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xy340, xy3700, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xy340), Just(xy3700), app(app(ty_Either, cg), da)) → new_esEs2(xy340, xy3700, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_@2, bd), be)) → new_esEs1(xy340, xy3700, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(app(ty_Either, bf), bg)) → new_esEs2(xy340, xy3700, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xy340), Just(xy3700), app(ty_[], cc)) → new_esEs(xy340, xy3700, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xy340), Just(xy3700), app(ty_Maybe, cd)) → new_esEs0(xy340, xy3700, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_Maybe, bc)) → new_esEs0(xy340, xy3700, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(xy341, xy3701, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(app(ty_@3, fg), fh), ga), eh) → new_esEs3(xy340, xy3700, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_@2, dh), ea)) → new_esEs1(xy341, xy3701, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_@2, fb), fc), eh) → new_esEs1(xy340, xy3700, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(app(ty_Either, fd), ff), eh) → new_esEs2(xy340, xy3700, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(app(ty_Either, eb), ec)) → new_esEs2(xy341, xy3701, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_[], df)) → new_esEs(xy341, xy3701, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_[], eg), eh) → new_esEs(xy340, xy3700, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), app(ty_Maybe, fa), eh) → new_esEs0(xy340, xy3700, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy340, xy341), @2(xy3700, xy3701), de, app(ty_Maybe, dg)) → new_esEs0(xy341, xy3701, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xy340), Left(xy3700), app(app(app(ty_@3, ha), hb), hc), gc) → new_esEs3(xy340, xy3700, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xy340), Right(xy3700), hd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy340, xy3700, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(xy342, xy3702, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(xy341, xy3701, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(xy340, xy3700, bea, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_@2, hg), hh)) → new_esEs1(xy340, xy3700, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xy340), Left(xy3700), app(app(ty_@2, ge), gf), gc) → new_esEs1(xy340, xy3700, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_@2, bcd), bce), bcb) → new_esEs1(xy341, xy3701, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_@2, bde), bdf), bag, bcb) → new_esEs1(xy340, xy3700, bde, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs1(xy342, xy3702, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), ba) → new_esEs(xy341, xy3701, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xy340, xy341), :(xy3700, xy3701), app(ty_[], bb)) → new_esEs(xy340, xy3700, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(xy340), Left(xy3700), app(app(ty_Either, gg), gh), gc) → new_esEs2(xy340, xy3700, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xy340), Right(xy3700), hd, app(app(ty_Either, baa), bab)) → new_esEs2(xy340, xy3700, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(app(ty_Either, bdg), bdh), bag, bcb) → new_esEs2(xy340, xy3700, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(app(ty_Either, bcf), bcg), bcb) → new_esEs2(xy341, xy3701, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(app(ty_Either, bbd), bbe)) → new_esEs2(xy342, xy3702, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(Left(xy340), Left(xy3700), app(ty_[], gb), gc) → new_esEs(xy340, xy3700, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_[], he)) → new_esEs(xy340, xy3700, he)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xy340), Left(xy3700), app(ty_Maybe, gd), gc) → new_esEs0(xy340, xy3700, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xy340), Right(xy3700), hd, app(ty_Maybe, hf)) → new_esEs0(xy340, xy3700, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_[], bah)) → new_esEs(xy342, xy3702, bah)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_[], bdc), bag, bcb) → new_esEs(xy340, xy3700, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_[], bca), bcb) → new_esEs(xy341, xy3701, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, app(ty_Maybe, bcc), bcb) → new_esEs0(xy341, xy3701, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), baf, bag, app(ty_Maybe, bba)) → new_esEs0(xy342, xy3702, bba)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy340, xy341, xy342), @3(xy3700, xy3701, xy3702), app(ty_Maybe, bdd), bag, bcb) → new_esEs0(xy340, xy3700, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy330, xy331), :(xy3710, xy3711), ba) → new_isPrefixOf(xy331, xy3711, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy330, xy331), :(xy3710, xy3711), ba) → new_isPrefixOf(xy331, xy3711, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf0(xy34, xy33, xy37, :(xy3610, xy3611), ba) → new_isPrefixOf0(xy34, xy33, new_flip(xy37, xy3610, ba), xy3611, ba)
The TRS R consists of the following rules:
new_flip(xy33, xy34, ba) → :(xy34, xy33)
The set Q consists of the following terms:
new_flip(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf0(xy34, xy33, xy37, :(xy3610, xy3611), ba) → new_isPrefixOf0(xy34, xy33, new_flip(xy37, xy3610, ba), xy3611, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 4, 5 >= 5
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf1(xy33, xy34, :(xy350, xy351), xy36, ba) → new_isPrefixOf1(new_flip(xy33, xy34, ba), xy350, xy351, xy36, ba)
The TRS R consists of the following rules:
new_flip(xy33, xy34, ba) → :(xy34, xy33)
The set Q consists of the following terms:
new_flip(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf1(xy33, xy34, :(xy350, xy351), xy36, ba) → new_isPrefixOf1(new_flip(xy33, xy34, ba), xy350, xy351, xy36, ba)
The graph contains the following edges 3 > 2, 3 > 3, 4 >= 4, 5 >= 5